Type Classes with Functional Dependencies

複数の型引数間の関係性をどう表現するか

2000/3

大まかな流れ

1 Introduction

なぜなら、型引数間の依存関係をcaputureできないから、という問題提議

2 Preliminaries: Type Classes in Haskell

型クラスの定義、型クラス制約、型クラスの継承、インスタンスなど基本的なことについて

3 Example: Building a Library of Collection Types

Collects型クラスを例に取って、実際にどういう問題が生じるのかを具体的に見る

code:hs

class Collects e ce where

empty :: ce -- 空のcollectionを作成

insert :: e -> ce -> ce -- 追加

member :: e -> ce -> Bool -- 存在確認

このクラス宣言には3つの問題が存在する

②型推論が正しくできないために、Collectsが異なる型の要素を持ててしまう

③コンパイルエラーは生じないが、実行時エラーが生じる

上述の①~③の問題を解決できる3つの解決案の提示

code:hs

class Collects e c where

empty :: c e

insert :: e -> c e -> c e

member :: e -> c e -> Bool

しかし、これは最初の定義ほど抽象的ではないため、最初の定義ではインスタンスにできた型のいくつかがインスタンスに取れなくなる

2つ目: パラメトリック多相な型クラスにする

code:hs

class ce ∈ Collects e where

empty :: ce

insert :: e -> ce -> ce

member :: e -> ce -> Bool

構文がキモいからか、何故か知らんがスルーされたらしい

3つ目: functional dependenciesを使う(本題)

code:hs

class Collects e c | c -> e where

empty :: c

insert :: e -> c -> c

member :: e -> c -> Bool

拡張構文としても良い感じ

4 Further Examples

有限集合の例の紹介

5 Relations and Functional Dependencies

6 Typing with Functional Dependencie

7 utting a Name to Functional Dependencies

8 Conclusions and Future Work

将来の作業

面白そうな関連論文

参考

この論文を軽く読んだっぽい人のブログ記事

読みメモ

A particular novelty of this paper is the application of ideasfrom the theory of relational databases to the design of type systems.

1 Introduction

More generally, functions in Haskell have types ofthe formP⇒τ, wherePis some list of predicates andτis a monotype. IfPis empty, then we usually abbreviateP⇒τasτ.

型クラスもカリー化できる

ということは複数の型引数を取りうる

という意味で、自然な一般化

So it is perhaps surprising that support for multiple parametertype classes is still not included in the Haskell standard, even in the most recentrevision . One explanation for this reticence is that some of the proposed applications have not worked particularly well in practice. These problems oftenoccur because the relations on types that we can specify using simple extensionsof Haskell are too general for practical applications. In particular, they fail tocapture important dependencies between parameters.

More concretely, the useof multiple parameter classes can often result in ambiguities and inaccuracies ininferred types, and in delayed detection of type errors

その理由は、これまでに提案されてきたアプリケーションのいくつかがちゃんと機能してないから

この型の関係は実際のアプリケーションには一般的すぎる

特に型引数間の依存関係をキャプチャできない

2 Preliminaries: Type Classes in Haskell

型クラスの定義、型クラス制約、型クラスの継承、インスタンスなど基本的なことについて

3 Example: Building a Library of Collection Types

Collection型クラスで複数引数の型クラスの問題を見る

Collectionを扱う型クラス

code:hs

class Collects e ce where

empty :: ce -- 空のcollectionを作成

insert :: e -> ce -> ce -- 追加

member :: e -> ce -> Bool -- 存在確認

例えば、List, characteristic functions, BitSet, hash tableとかが、インスタンスになる

code:hs

empty = []

insert = (:)

member = elem

このクラス宣言には3つの問題が存在する

右辺に出てこない型が左辺に存在することを「曖昧」と読んでいる

無理やり解決する方法は、emptyの定義をCollectsの定義から消すこと

The problem with this is that, accordingto the theoretical foundations of Haskell overloading, we cannot guarantee a well-defined semantics for any term with an ambiguous type

この辺に書いてるらしい

②Collectsが異なる型の要素を持ててしまう

code:hs

f x y coll = insert x $ insert y coll

g coll = f True 'a' coll

これは以下のように推論されて型検査を通過してしまう

code:hs

f :: (Collects a c, Collects b c) => a -> b -> c -> c

g :: (Collects Bool c, Collects Char c) => c -> c

Collectsは同じ型のCollectionがほしかったはずなのにこれでは都合が悪い

③これらの関数は定義時には型エラーが出ないが、実行時に都合がわるいことになる

よって、どうにかして

型の曖昧さの排除

正しい型推論

型エラーの早期検出

つまり、定義時に間違いにきづけるように

したい

1詰めの解決法

code:hs

class Collects e c where

empty :: c e

insert :: e -> c e -> c e

member :: e -> c e -> Bool

リストで言えば、

これで上の3つの問題は解決する

しかし、これまた問題がある

先の4つの例の内、Listしかinstanceにできない

2つ目の解決法

パラメトリック多相な型クラスにする

PTCと呼んでる

parametric type classes

code:hs

class ce ∈ Collects e where

empty :: ce

insert :: e -> ce -> ce

member :: e -> ce -> Bool

What makes it different from the two parameter class in Sec-tion 3 is the implied assumption that the element type e is uniquely determinedby the collection type ce.

上の①~③のような問題も起きない

定義の構文の問題などでスルーされたらしい

In part, this may be because it was seen,incorrectly, as an alternative to constructor classes and not, more accurately,as an orthogonal extension.

functional dependenciesを使う

code:hs

class Collects e c | c -> e where

empty :: c

insert :: e -> c -> c

member :: e -> c -> Bool

拡張構文としてもマシ

型クラスの定義のみの変更であって、instance宣言や型クラス制約には影響がない

例

code:hs

class C a b where ..

class D a b | a -> b where ..

class E a b | a -> b, b -> a where ..

Cは二項関係

Dは、(部分)関数であることを示す

それよりも制限がかかっている

Eは、全単射であることを示す

こうすれば、以下の様に書くとエラーになる

なる、というか、コンパイラはエラーにしないといけない

code:hs

instance D Bool Int where ...

instance D Bool Char where ...

どちらか片方の定義なら許容するが、両方の定義は許容されない

これもエラー

code:hs

section4

さらなる例

code:hs

class Mul a b c | a b -> c where

(*) :: a -> b -> c

instance Mul Int Int Int where ..

instance Mul Int Float Float where ..

instance Mul Float Int Float where ..

instance Mul Float Float Float where ..

(1 * 2) * 3 :: (Mul Int Int a, Mul a Int b) => b

fun depsの情報があるおかけでちゃんと推論される

有限集合の例など

section5

fun depsの基本理論

section6

型推論の理論の話

section7

we describe some further opportunities for using dependency information

さらなるお話

fun depsした型クラスを継承した時とかの話

section8

将来の作業